p:, q:int_nzero, a,b:.
coprime(p; q)
 coprime(a; b)
 ((p * b) = (a * q))
 ((p < 0)  (a < 0))
 ((q < 0)  (b < 0))
 (<p, q> = <a, b>  (:  int_nzero)) 

latex

Definitions	prop{i:l}, nequal(T; a; b), t  T, P  Q, P  Q, P  Q, int_nzero, x:A. B(x), False, A, guard(T)
Lemmas	int nzero wf, coprime wf, iff wf, nequal wf, coprime-equiv-unique